package org.xteam.sled.model;

import org.xteam.sled.semantic.exp.Exp;
import org.xteam.sled.semantic.exp.ExpBindingInstance;
import org.xteam.sled.semantic.exp.ExpInstanceInput;
import org.xteam.sled.semantic.exp.ExpInstanceTagged;
import org.xteam.sled.semantic.exp.ExpVar;
import org.xteam.sled.semantic.exp.IExpRewriter;

public class LatentLabel extends Label implements ILatentSequent, ILabelledSequent {
	
	private Exp exp;

	public LatentLabel(Exp exp) {
		this.exp = exp;
	}

	@Override
	public ISequent merge(ISequent o) {
		throw new RuntimeException("should not be called");
	}

	public ILabelledSequent injectLatent() {
		return this;
	}
	
	@Override
	public ISequent subs(IExpRewriter subs) {
		return new LatentLabel(subs.rewrite(exp));
	}

	@Override
	public ILabelledSequent actualize(boolean actualsOk) {
		if (exp instanceof ExpBindingInstance) {
			ExpBindingInstance bi = (ExpBindingInstance) exp;
			if (actualsOk) {
				if (bi.wild())
					return null;
				return new ActualLabel(bi.name());
			} else
				throw new RuntimeException("latent label becoming actual");
		} else if (isIgnorable(exp)) {
			return null;
		} else {
			throw new RuntimeException("type of latent-label expression");
		}
	}
	
	private static boolean isIgnorable(Exp e) {
		if (e instanceof ExpVar)
			return true;
		if (e instanceof ExpInstanceTagged) // XXX
			return true;
		if (e instanceof ExpInstanceInput) {
			return isIgnorable(((ExpInstanceInput) e).getExpr());
		}
		return false;
	}
	
	@Override
	public String toString() {
		return exp + ":";
	}
	
}
